FDL - Nuprl Definition : sframe-p

Nuprl Definition : sframe-p

0,22

only events in L send on l with tg ==

e:E. kind(e) = rcv(l,tg)

(kind(sender(e))

clarification:

sframe-p(es;l;tg;L)
==

e:es-E(es). es-kind(es; e) = rcv(l,tg)

Knd

(es-kind(es; es-sender(es; e))

Knd)

Definitions x:A. B(x), E, P Q, rcv(l,tg), (x l), kind(e), sender(e), Knd

FDL editor aliases sframe-p

Definitions	x:A. B(x), E, P Q, rcv(l,tg), (x l), kind(e), sender(e), Knd
FDL editor aliases	sframe-p